Embedded devices are becoming pervasive and playing increasing role in our lives. We depend on cell phones and ATMs. Embedded systems are also used in mission critical applications such as aircraft navigation and control systems, heart pacemaker devices, and military systems. Correct functioning of these devices is crucial. To establish correctness, subjecting them to various possible inputs tests these devices. However, exhaustive testing is not only costly and time consuming but also impossible for non-trivial devices. A complementary approach is to apply static model checking techniques to verify that the design of a device holds certain correctness properties.
Model Checking is used to establish correctness of a given program. Model Checking techniques typically convert program constructs in a program into equivalent mathematical logic or constructs. These mathematical constructs collectively define the underlying mathematical model of the program. In essence, the mathematical model defines the various states a given program can be in, and the conditions (inputs) required for various state transitions.
The correctness is established by exploring the state space of the mathematical model and verifying that none of the execution paths will lead to a program state that violates one or more constraints from a pre-defined constraint set.
Evidently, the correctness proof of a program with any Model Checking technique is based on the assumption that the translation of a program to a mathematical model is flawless. If the translation is incorrect, then the correctness proof is unreliable. That is why it is very important that the translation is correct without a doubt.
Model Checking techniques are very useful in embedded devices that have real-time software. In such devices, all possible inputs cannot be tested, but the correctness of software is vital because these devices have critical applications such as health and military applications. Real time systems are concurrent reactive systems represented by communicating state machines. The communication channels between state machines are defined using Priority Message Queue programming construct.
The embedded devices fall into the category of concurrent reactive systems and their design can be expressed through Unified Modeling Language (UML) state machines communicating with each other through signal and message passing. For static model checking, the UML state machines have to be converted into modeling languages suitable for model checking. A challenging aspect of the conversion is efficient modeling of communication channels between the state machines. This aspect is difficult because the scalability of model checking techniques is limited due to the problem of state space explosion. A channel is essentially a non-deterministic priority message queue. The model should be expressive enough to capture the behavior of a non-deterministic priority queue, yet the possible permutations should occupy small state space.
Existing techniques to model priority queues typically have a single queue, and allow each cell to swap its content with the cell before it depending upon the different priorities of the cells. Though this model is concise (i.e. less bits to model), the behavior is complex (i.e. model of each bit is complex). For symbolic model checking, the behavior needs to be encoded into a representation suitable for model checking (such as SAT (Satisfiability problem) or BDD (Binary Decision Diagram)). Complex behavior results in bigger encoding. Therefore, the complexity of the behavior is an important issue for performing model checking.